@i stable state.P(state)   == e@i. P((discrete state when e))  P((discrete state after e)) 

latex

---

clarification:

es-stable(es;i;state.P(state))
== alle-at(es;i;e.P(es-dstate-when(es;e))  P(es-dstate-after(es;e))) 

latex

Definitions	e@i. P(e), P  Q, (discrete state when e), (discrete state after e)
FDL editor aliases	es-stable